Nuprl Lemma : Raframe_wf
0,22
postcript
pdf
loc
:Id,
k
:Knd,
L
:Id List. @
loc
:
k
writes only members of
L
Realizer
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Realizer
,
@
loc
:
k
writes only members of
L
,
Prop
,
x
.
t
(
x
)
,
x
(
s
)
Lemmas
IdLnk
wf
,
Id
wf
,
fpf
wf
,
decl-state
wf
,
Knd
wf
,
decl-type
wf
,
unit
wf
origin